Inference at * 2 2 2 1 1 
Iof proof for Lemma adjacent-append:



1. T : Type
2. x : T
3. y : T
4. L1 : T List
5. u : T
6. v : T List
7. 0 < ||L1||
8. 0 < (||v||+1)
9. x = last(L1)
10. y = u
  y = [u / v][(((||L1|| - 1)+1) - ||L1||)] 

latex

 by ((RWO "select_cons_hd" 0) 
CollapseTHEN (Auto')) 

latex

C.

Definitions	l[i], P  Q, P & Q, x:A  B(x), P  Q, P  Q, n+m, n - m, ||as||, x:A. B(x), x:AB(x), A  B, , last(L), t  T, #$n, s = t, a < b, type List, Type
Lemmas	iff wf, rev implies wf, select cons hd, length wf1